Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    f(f(X,Y),Z)  → f(X,f(Y,Z))
2:    f(X,f(Y,Z))  → f(Y,Y)
There are 3 dependency pairs:
3:    F(f(X,Y),Z)  → F(X,f(Y,Z))
4:    F(f(X,Y),Z)  → F(Y,Z)
5:    F(X,f(Y,Z))  → F(Y,Y)
Consider the SCC {3-5}. The constraints could not be solved.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 3, 2006